Abstract state machines provide models for testing program behavior. See Executable Specifications: Creating Testable, Enforceable Designs, Microsoft Research, Feb. 9, 2001. An abstract state machine language provides language constructs for describing desirable program behavior. See Gurevich, et al., Toward Industrial Strength Abstract State Machines, Microsoft Research, October 2001. These language constructs are compiled into a verifiable model of program behavior including states and state transitions. Programs are exercised and verified against a model, and non-determinism is discussed as bounded sets. See Barnett, et al., Spying on Components: A Runtime Verification Technique, Microsoft Research, October 2001. Abstract state machines are used to generate tests for verifying programs. See Generating Finite State Machines from Abstract State Machines, Grieskamp, et al., Microsoft Research, May 2002. A Chinese Postman Tour is described for providing coverage of a deterministic finite state machine modeling program behavior. Id. However, some programs such as network protocols and distributed applications, depend on external behavior. There is presently no method for modeling or verifying program behavior that includes traversing and providing coverage to vertices or edges reachable through a non-deterministic graph.